Example 2 in [Lucas - IC'02]

Summary: Ex2_Luc02a

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (LPO @ AProVE)
  2. Zantema's transformation (RPOS @ AProVE)
  3. Ferreira and Ribeiro's transformation (Corollary)
  4. Giesl and Middeldorp's transformation (Corollary)
  5. CSRPO
  6. CSDP

CS-TRS Ex2_Luc02a (file Ex2_Luc02a.csr)

Functions:  terms cons recip sqr s 0 add dbl first nil

Constructors:  cons recip s 0 nil

Variables:  N X Y Z

Arities: 

ar(terms) = 1
ar(cons) = 2
ar(recip) = 1
ar(sqr) = 1
ar(s) = 1
ar(0) = 0
ar(add) = 2
ar(dbl) = 1
ar(first) = 2
ar(nil) = 0

Replacement map: 

µ(terms)={1}
µ(cons)={1}
µ(recip)={1}
µ(sqr)={1}
µ(s)={1}
µ(0)={}
µ(add)={1,2}
µ(dbl)={1}
µ(first)={1,2}
µ(nil)={}

Rules:  (file Ex2_Luc02a)   

terms(N) -> cons(recip(sqr(N)),terms(s(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X),dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
first(0,X) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))

The CS-TRS in OBJ format (file Ex2_Luc02a.obj):

obj Ex2_Luc02a is
  sort S .
  op terms : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op recip : S -> S .
  op sqr : S -> S .
  op s : S -> S .
  op 0 : -> S .
  op add : S S -> S .
  op dbl : S -> S .
  op first : S S -> S .
  op nil : -> S .
  vars N X Y Z : S .
  eq terms(N) = cons(recip(sqr(N)),terms(s(N))) .
  eq sqr(0) = 0 .
  eq sqr(s(X)) = s(add(sqr(X),dbl(X))) .
  eq dbl(0) = 0 .
  eq dbl(s(X)) = s(s(dbl(X))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq first(0,X) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
endo

Negative results

Positive results

1. Ex2_Luc02a is proved µ-terminating in [Luc02a, Example 3] by using Lucas' transformation. The TRS Ex2_Luc02a_L:

       terms(N) -> cons(recip(sqr(N)))
       sqr(0) -> 0
       sqr(s(X)) -> s(add(sqr(X),dbl(X)))
       dbl(0) -> 0
       dbl(s(X)) -> s(s(dbl(X)))
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       first(0,X) -> nil
       first(s(X),cons(Y)) -> cons(Y)
       

   is terminating (use LPO with AProVE).
2. The µ-termination of Ex2_Luc02a can be proved by using Zantema's transformation. The TRS Ex2_Luc02a_Z:

       terms(N) -> cons(recip(sqr(N)),n__terms(s(N)))
       sqr(0) -> 0
       sqr(s(X)) -> s(add(sqr(X),dbl(X)))
       dbl(0) -> 0
       dbl(s(X)) -> s(s(dbl(X)))
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       first(0,X) -> nil
       first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
       terms(X) -> n__terms(X)
       first(X1,X2) -> n__first(X1,X2)
       activate(n__terms(X)) -> terms(X)
       activate(n__first(X1,X2)) -> first(X1,X2)
       activate(X) -> X
       

   is terminating (use RPOS with AProVE).
3. By [GM04, Theorem 11], the µ-termination of Ex2_Luc02a can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
4. By [GM04, Theorem 22], the µ-termination of Ex2_Luc02a can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
5. The µ-termination of Ex2_Luc02a can be proved by using CSRPO (proof due to Albert Rubio)and automatically by MuTerm:
   • marking map:

            m(cons,2)={terms}
            

   • precedence:

            terms > cons, recip, sqr, terms', s
            sqr > s, add, dbl
            dbl > s
            add > s
            first > nil, cons, terms
            

   • status:

            st(first) = lex
            

6. The µ-termination of Ex2_Luc02a can be proved by using CSDP (computed by MuTerm).